/* Soot - a J*va Optimization Framework
 * Copyright (C) 2003 Jerome Miecznikowski
 * Copyright (C) 2004-20055 Nomair A. Naeem
 *
 * This library is free software; you can redistribute it and/or
 * modify it under the terms of the GNU Lesser General Public
 * License as published by the Free Software Foundation; either
 * version 2.1 of the License, or (at your option) any later version.
 *
 * This library is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
 * Lesser General Public License for more details.
 *
 * You should have received a copy of the GNU Lesser General Public
 * License along with this library; if not, write to the
 * Free Software Foundation, Inc., 59 Temple Place - Suite 330,
 * Boston, MA 02111-1307, USA.
 */

package soot.dava.toolkits.base.finders;

import soot.*;
import soot.dava.*;
import soot.util.*;

import java.util.*;

import soot.jimple.*;
import soot.toolkits.graph.*;
import soot.dava.internal.asg.*;
import soot.dava.internal.SET.*;

public class SynchronizedBlockFinder implements FactFinder {
	public SynchronizedBlockFinder(Singletons.Global g) {
	}

	public static SynchronizedBlockFinder v() {
		return G.v().soot_dava_toolkits_base_finders_SynchronizedBlockFinder();
	}

	private HashMap<AugmentedStmt, Map<Value, Integer>> as2ml;
	private DavaBody davaBody;

	/*
	 * Nomair A Naeem 08-FEB-2005 monitorLocalSet contains all the locals that
	 * are used in monitors monitorEnterSet contains all enterMonitorStmts
	 * Statements
	 */
	private IterableSet monitorLocalSet, monitorEnterSet;

	private final Integer WHITE = new Integer(0);// never visited in DFS
	private final Integer GRAY = new Integer(1);// visited but not finished
	private final Integer BLACK = new Integer(2);// finished

	private final int UNKNOWN = -100000; // Note there are at most 65536 monitor
											// exits in a method.
	private final Integer VARIABLE_INCR = new Integer(UNKNOWN);

	private final String THROWABLE = "java.lang.Throwable";

	public void find(DavaBody body, AugmentedStmtGraph asg, SETNode SET)
			throws RetriggerAnalysisException {
		davaBody = body;
		Dava.v().log("SynchronizedBlockFinder::find()");

		as2ml = new HashMap();

		IterableSet synchronizedBlockFacts = body.get_SynchronizedBlockFacts();
		synchronizedBlockFacts.clear();

		set_MonitorLevels(asg);

		Map<AugmentedStmt, IterableSet> as2synchSet = build_SynchSets();

		IterableSet usedMonitors = new IterableSet();

		AugmentedStmt previousStmt = null;

		Iterator asgit = asg.iterator();
		while (asgit.hasNext()) {
			// going through all augmentedStmts

			AugmentedStmt as = (AugmentedStmt) asgit.next();
			if (as.get_Stmt() instanceof EnterMonitorStmt) {
				// for each monitor enter stmt found

				IterableSet synchSet = as2synchSet.get(as);
				if (synchSet != null) {
					IterableSet synchBody = get_BodyApproximation(as, synchSet);
					Value local = ((EnterMonitorStmt) as.get_Stmt()).getOp();
					Value copiedLocal = null;

					/*
					 * Synch bug due to copy stmts r2 = r1 enter monitor r1
					 * synch body exit monitor r2 we need to realize that r1 and
					 * r2 are the same implemented as a hack, the correct
					 * approach is reaching copies
					 */
					if (previousStmt != null) {
						Stmt previousS = previousStmt.get_Stmt();
						if (previousS instanceof DefinitionStmt) {
							DefinitionStmt previousDef = (DefinitionStmt) previousS;
							Value rightPrevious = previousDef.getRightOp();
							if (rightPrevious.toString().compareTo(
									local.toString()) == 0) {
								copiedLocal = previousDef.getLeftOp();
							}
						}
					}

					Integer level = as2ml.get(as).get(local);
					Iterator enit = body.get_ExceptionFacts().iterator();

					// going through all exception nodes in the DavaBody
					boolean done = false;
					IterableSet origSynchBody = synchBody;
					while (enit.hasNext()) {
						ExceptionNode en = (ExceptionNode) enit.next();
						synchBody = (IterableSet) origSynchBody.clone();
						// see if the two bodies match exactly

						if (verify_CatchBody(en, synchBody, local, copiedLocal)) {
							if (SET.nest(new SETSynchronizedBlockNode(en, local))) {
								done = true;
								// System.out.println("synch block created");
								Iterator ssit = synchSet.iterator();
								while (ssit.hasNext()) {
									AugmentedStmt ssas = (AugmentedStmt) ssit
											.next();
									Stmt sss = ssas.get_Stmt();

									/*
									 * Jeromes Implementation: changed because
									 * of copy stmt bug
									 * 
									 * if ((sss instanceof MonitorStmt) &&
									 * (((MonitorStmt) sss).getOp() == local) &&
									 * (((Integer) ((HashMap) as2ml.get(
									 * ssas)).get( local)).equals( level)) &&
									 * (usedMonitors.contains( ssas) == false)){
									 */
									if (sss instanceof MonitorStmt) {
										if ((((MonitorStmt) sss).getOp() == local)
												&& ((as2ml.get(ssas).get(local))
														.equals(level))
												&& (usedMonitors.contains(ssas) == false)) {

											usedMonitors.add(ssas);
										} else {
											if ((((MonitorStmt) sss).getOp() == copiedLocal)
													&& (usedMonitors
															.contains(ssas) == false)) {
												// note we dont check levels in
												// this case
												usedMonitors.add(ssas);
											}
										}
									}
								}
								synchronizedBlockFacts.add(en);
							}
							break;
						} else {
							// throw new
							// RuntimeException("Could not verify approximated Synchronized body");
						}
					}
					if (!done)
						throw new RuntimeException(
								"Could not verify approximated Synchronized body!\n"
										+ "Method:\n"
										+ body.getMethod()
										+ "Body:\n"
										+ "===============================================================\n"
										+ body.getUnits()
										+ "===============================================================\n");
				}// non null synch set for this enter monitor stmt
			}// if the augmented stmt was a enter monitor stmt
			previousStmt = as;
		}// going through all augmented stmts

		IterableSet<AugmentedStmt> monitorFacts = body.get_MonitorFacts();
		monitorFacts.clear();

		for (AugmentedStmt as : asg) {
			if ((as.get_Stmt() instanceof MonitorStmt)
					&& (usedMonitors.contains(as) == false)) {
				monitorFacts.add(as);
			}
		}
	}

	/*
	 * as2locals: contains all locals which have unknown level for this
	 * augmented stmt viAugStmts: contains all augmented stmts which have some
	 * unknown level local in them
	 */

	private void find_VariableIncreasing(AugmentedStmtGraph asg,
			HashMap local2level_template, LinkedList<AugmentedStmt> viAugStmts,
			HashMap<AugmentedStmt, LinkedList<Value>> as2locals) {
		StronglyConnectedComponentsFast scc = new StronglyConnectedComponentsFast(
				asg);
		IterableSet viSeeds = new IterableSet();
		HashMap as2color = new HashMap(), as2rml = new HashMap();

		// as2rml contains each augmented stmt as key with a local2Level mapping
		// as value
		Iterator asgit = asg.iterator();
		while (asgit.hasNext()) {
			as2rml.put(asgit.next(), local2level_template.clone());
		}

		// loop through all the strongly connected components in the graph
		Iterator<List> sccit = scc.getTrueComponents().iterator();
		while (sccit.hasNext()) {
			// componentList contains augmentedstmts belonging to a particular
			// scc
			List componentList = sccit.next();

			// component contains augmentedstmts belonging to a particular scc
			IterableSet component = new IterableSet();
			component.addAll(componentList);

			// add to as2color each augstmt belonging to the component as the
			// key and the color white as the value
			Iterator cit = component.iterator();
			while (cit.hasNext()) {
				as2color.put(cit.next(), WHITE);
			}

			// DFS and mark enough of the variable increasing points to get
			// started.
			AugmentedStmt seedStmt = (AugmentedStmt) component.getFirst();
			// seedStmt contains the first stmt of the scc

			DFS_Scc(seedStmt, component, as2rml, as2color, seedStmt, viSeeds);
			// viSeeds contain augmentedStmts which have unknown level since
			// their level was less
			// than that of their predecessors
		}

		// viSeeds contains all the augmentedStmts with unknown level in the
		// method (for all scc)
		IterableSet worklist = new IterableSet();
		worklist.addAll(viSeeds);

		// Propegate the variable increasing property.
		while (worklist.isEmpty() == false) {
			AugmentedStmt as = (AugmentedStmt) worklist.getFirst();
			worklist.removeFirst();
			HashMap local2level = (HashMap) as2rml.get(as);

			// get all sucessors of the viSeed
			Iterator sit = as.csuccs.iterator();
			while (sit.hasNext()) {
				AugmentedStmt sas = (AugmentedStmt) sit.next();
				HashMap<Value, Integer> slocal2level = (HashMap<Value, Integer>) as2rml
						.get(sas);

				Iterator mlsit = monitorLocalSet.iterator();
				while (mlsit.hasNext()) {
					Value local = (Value) mlsit.next();

					// if the level for a local is set to unknown and the level
					// for the same local is not
					// set to unknown in the successor set it and add it to the
					// worklist
					if ((local2level.get(local) == VARIABLE_INCR)
							&& (slocal2level.get(local) != VARIABLE_INCR)) {
						slocal2level.put(local, VARIABLE_INCR);

						if (worklist.contains(sas) == false)
							worklist.addLast(sas);
					}
				}
			}
		}
		/*
		 * At the end of this the worklist is empty the unknown level of locals
		 * of an augmentedstmt present in the viSeed has been propagated through
		 * out the stmts reachable from that stmt
		 */

		// Summarize the variable increasing information for the
		// set_MonitorLevels() function.
		asgit = asg.iterator();
		while (asgit.hasNext()) {
			AugmentedStmt as = (AugmentedStmt) asgit.next();
			HashMap local2level = (HashMap) as2rml.get(as);

			Iterator mlsit = monitorLocalSet.iterator();
			while (mlsit.hasNext()) {
				// for each local involved in monitor stmts
				Value local = (Value) mlsit.next();

				if (local2level.get(local) == VARIABLE_INCR) {

					/*
					 * Nomair A. Naeem 08-FEB-2005 BUG IN CODE. The getLast
					 * method returns a NoSuchElementException if list is empty.
					 * Protect this by checking isEmpty
					 */
					if (!viAugStmts.isEmpty()) {
						if (viAugStmts.getLast() != as)
							viAugStmts.addLast(as);
					} else {
						// System.out.println("List was empty added as");
						viAugStmts.addLast(as);
					}

					LinkedList<Value> locals = null;

					if ((locals = as2locals.get(as)) == null) {
						locals = new LinkedList<Value>();
						as2locals.put(as, locals);
					}

					locals.addLast(local);
				}
			}
		}
	}

	/*
	 * Inputs: as: the seed stmt, i.e. the first statement of a strongly
	 * connected component component: the strongly connected stmt being
	 * processed as2rml: a hashmap which contains an augmentedstmt as key and a
	 * hashmap with local to level mapping as value as2color: maps each
	 * augmentedstmt of a scc to a color (white initially) viSeeds: variable
	 * increasing levels, initially empty
	 * 
	 * Purpose: makes a traversal of the entire scc and increases the levels of
	 * locals when used in monitor enter decreases the levels of locals when
	 * leaving monitor if a successor has never been visited invoke same method
	 * on it with updated level information if a sucessor has been visited
	 * before and has a lower level than a seed the level of the sucessor is
	 * marked unknown and is added to the viSeeds list
	 */
	private void DFS_Scc(AugmentedStmt as, IterableSet component,
			HashMap as2rml, HashMap as2color, AugmentedStmt seedStmt,
			IterableSet viSeeds) {
		as2color.put(as, GRAY);

		Stmt s = as.get_Stmt();
		// get local to level mapping of the augmented stmt
		HashMap<Value, Integer> local2level = (HashMap<Value, Integer>) as2rml
				.get(as);

		if (s instanceof MonitorStmt) {
			Value local = ((MonitorStmt) s).getOp();

			if (s instanceof EnterMonitorStmt) {// its an enter hence increase
												// level for this local
				local2level.put(local, new Integer(local2level.get(local)
						.intValue() + 1));
			} else {// its an exit stmt hence reduce level
				local2level.put(local, new Integer(local2level.get(local)
						.intValue() - 1));
			}
		}

		// get all successors of the augmented stmt
		Iterator sit = as.csuccs.iterator();
		// going through sucessors
		while (sit.hasNext()) {
			AugmentedStmt sas = (AugmentedStmt) sit.next();

			if (component.contains(sas) == false)
				continue;

			// get the local2Level hashmap for the successor
			HashMap<Value, Integer> slocal2level = (HashMap<Value, Integer>) as2rml
					.get(sas);
			// get the color for the sucessor
			Integer scolor = (Integer) as2color.get(sas);

			if (scolor.equals(WHITE)) {
				// the augmented stmt hasnt been handled yet
				Iterator mlsit = monitorLocalSet.iterator();
				while (mlsit.hasNext()) {
					// for all locals which are used in monitor stmts
					Value local = (Value) mlsit.next();
					/*
					 * update the sucessors hashtable with level values from the
					 * seed stmt The loca2Level is the hashmap of local-->level
					 * for the seed The sLocal2Level is the hashmap of local -->
					 * level for the successor of the seed
					 */
					slocal2level.put(local, local2level.get(local));
				}

				// do recursive call on the sucessor
				DFS_Scc(sas, component, as2rml, as2color, seedStmt, viSeeds);
			}

			else {
				// if the augmented stmt has been visited before
				Iterator mlsit = monitorLocalSet.iterator();
				while (mlsit.hasNext()) {
					Value local = (Value) mlsit.next();

					if (slocal2level.get(local).intValue() < local2level.get(
							local).intValue()) {
						// if the sucessors value for the level of a local is
						// less than that of the level of the seed
						// make the level for this local to be unknown-->
						// VARIABLE_INCR
						slocal2level.put(local, VARIABLE_INCR);

						// add this to the viSeeds list
						if (viSeeds.contains(sas) == false)
							viSeeds.add(sas);
					}
				}
			}
		}

		// mark augmented stmt as done
		as2color.put(as, BLACK);
	}

	/*
	 * Created a synch set for each enter monitor stmt. The synch set contains
	 * all sucessors of the monitor enter stmt which is dominated by the enter
	 * stmt and the level is greater or equal to that of the enter stmt
	 */
	private Map<AugmentedStmt, IterableSet> build_SynchSets() {
		HashMap<AugmentedStmt, IterableSet> as2synchSet = new HashMap<AugmentedStmt, IterableSet>();

		Iterator mesit = monitorEnterSet.iterator();
		monitorEnterLoop: while (mesit.hasNext()) {
			// going through monitor enter stmts
			AugmentedStmt headAs = (AugmentedStmt) mesit.next();
			Value local = ((EnterMonitorStmt) headAs.get_Stmt()).getOp();
			IterableSet synchSet = new IterableSet();

			// get the monitor level for the local uses in the enter stmt
			int monitorLevel = (as2ml.get(headAs).get(local)).intValue();
			IterableSet worklist = new IterableSet();
			worklist.add(headAs);

			while (worklist.isEmpty() == false) {
				AugmentedStmt as = (AugmentedStmt) worklist.getFirst();
				worklist.removeFirst();

				Stmt s = as.get_Stmt();
				if ((s instanceof DefinitionStmt)
						&& (((DefinitionStmt) s).getLeftOp() == local))
					continue monitorEnterLoop;

				synchSet.add(as);

				Iterator sit = as.csuccs.iterator();
				while (sit.hasNext()) {
					AugmentedStmt sas = (AugmentedStmt) sit.next();
					// get the sucessors monitor level
					int sml = (as2ml.get(sas).get(local)).intValue();

					/*
					 * if the sucessor is dominated by the head stmt and the
					 * level is greater or equal to that of the head and is not
					 * waiting to be analysed and is not in the synchSet.. then
					 * add it to worklist
					 */
					if (sas.get_Dominators().contains(headAs)
							&& (sml >= monitorLevel)
							&& (worklist.contains(sas) == false)
							&& (synchSet.contains(sas) == false))

						worklist.addLast(sas);
				}
			}

			as2synchSet.put(headAs, synchSet);
		}
		return as2synchSet;
	}

	/*
	 * MonitorLocalSet: contains all locals used in monitor enter statements
	 * MonitorEnterSet: contains all monitor enter statements as2ml : key is
	 * each augmented stmt of the augmented graph, value is a hashmap which
	 * contains a local as key and the level as value
	 */
	private void set_MonitorLevels(AugmentedStmtGraph asg) {
		monitorLocalSet = new IterableSet();
		monitorEnterSet = new IterableSet();

		// Identify the locals that are used in monitor statements, and all the
		// monitor enters.
		Iterator<AugmentedStmt> asgit = asg.iterator();
		while (asgit.hasNext()) {
			AugmentedStmt as = asgit.next();
			Stmt s = as.get_Stmt();

			if (s instanceof MonitorStmt) {
				Value local = ((MonitorStmt) s).getOp();

				// if the monitorLocalSet does not contain this local add it
				if (monitorLocalSet.contains(local) == false)
					monitorLocalSet.add(local);

				// add the monitor enter statement to the monitorEnter Set
				if (s instanceof EnterMonitorStmt)
					monitorEnterSet.add(as);
			}
		}

		// Set up a base monitor lock level of 0 for all monitor locals.
		HashMap local2level_template = new HashMap();
		Iterator mlsit = monitorLocalSet.iterator();
		while (mlsit.hasNext()) {
			// add the local as key and value 0 as value
			local2level_template.put(mlsit.next(), new Integer(0));
		}

		// Give each statement the base monitor lock levels.
		asgit = asg.iterator();
		while (asgit.hasNext()) {
			// the augmented stmt is key and the whole hashMap with all the
			// local-->value mapping is the key
			as2ml.put(asgit.next(),
					(Map<Value, Integer>) local2level_template.clone());
		}

		LinkedList<AugmentedStmt> viAugStmts = new LinkedList<AugmentedStmt>();
		HashMap<AugmentedStmt, LinkedList<Value>> incrAs2locals = new HashMap<AugmentedStmt, LinkedList<Value>>();

		// setup the variable increasing monitor levels
		find_VariableIncreasing(asg, local2level_template, viAugStmts,
				incrAs2locals);
		/*
		 * At this time the viAugStmts contains all augments Stmt which have
		 * some local that has unknown level the incrAs2locals contains a map of
		 * augmented stmt to a linkedlist which contains locals with unknown
		 * level
		 */

		// going through all augmented stmts with some local with unknown level
		Iterator<AugmentedStmt> viasit = viAugStmts.iterator();
		while (viasit.hasNext()) {
			AugmentedStmt vias = viasit.next();
			Map local2level = as2ml.get(vias);

			// getting the list of locals with unknown level for this augmented
			// stmt
			Iterator lit = incrAs2locals.get(vias).iterator();
			while (lit.hasNext()) {
				// marking the level for this local as unknown
				local2level.put(lit.next(), VARIABLE_INCR);
			}
		}

		IterableSet worklist = new IterableSet();
		worklist.addAll(monitorEnterSet);

		// Flow monitor lock levels.
		while (worklist.isEmpty() == false) {
			// going through all monitor enter stmts
			AugmentedStmt as = (AugmentedStmt) worklist.getFirst();
			worklist.removeFirst();

			Map<Value, Integer> cur_local2level = as2ml.get(as);

			Iterator pit = as.cpreds.iterator();
			while (pit.hasNext()) {
				// going through preds of an enter monitor stmt
				AugmentedStmt pas = (AugmentedStmt) pit.next();
				Stmt s = as.get_Stmt();

				Map pred_local2level = as2ml.get(pas);

				mlsit = monitorLocalSet.iterator();
				while (mlsit.hasNext()) {
					Value local = (Value) mlsit.next();

					int predLevel = ((Integer) pred_local2level.get(local))
							.intValue();
					Stmt ps = pas.get_Stmt();

					if (predLevel == UNKNOWN) // Already marked as variable
												// increasing.
						continue;

					if (ps instanceof ExitMonitorStmt) {

						ExitMonitorStmt ems = (ExitMonitorStmt) ps;
						/*
						 * if the predecessor stmt is a monitor exit and the
						 * local it exits is the same as this local and the
						 * predLevel is greater than 0 decrease the pred level
						 */
						if ((ems.getOp() == local) && (predLevel > 0))
							predLevel--;
					}

					if (s instanceof EnterMonitorStmt) {
						EnterMonitorStmt ems = (EnterMonitorStmt) s;
						/*
						 * if the stmt is a monitor enter (which is true for the
						 * initial worklist) and the local it enters is the same
						 * as this local and the predLevel is greater or equal
						 * to 0 increase the pred level
						 */
						if ((ems.getOp() == local) && (predLevel >= 0))
							predLevel++;
					}

					int curLevel = cur_local2level.get(local).intValue();

					/*
					 * if the pred level is greater than the current level
					 * update current level add the sucessors of the stmt to the
					 * worklist
					 */
					if (predLevel > curLevel) {
						cur_local2level.put(local, new Integer(predLevel));

						Iterator sit = as.csuccs.iterator();
						while (sit.hasNext()) {
							Object so = sit.next();

							if (worklist.contains(so) == false)
								worklist.add(so);
						}
					}
				}
			}
		}
	}

	/*
	 * If a stmt is removed from the synchBody then all other stmts which are
	 * dominated by this stmt should also be removed from the synchBody
	 */
	private void removeOtherDominatedStmts(IterableSet synchBody,
			AugmentedStmt sas) {
		ArrayList toRemove = new ArrayList();

		Iterator it = synchBody.iterator();
		while (it.hasNext()) {
			AugmentedStmt as = (AugmentedStmt) it.next();
			IterableSet doms = as.get_Dominators();
			if (doms.contains(sas)) {
				// System.out.println("\n\nstmt:"+as+" is dominated by removed stmt"+sas);
				toRemove.add(as);
			}
		}

		it = toRemove.iterator();
		while (it.hasNext()) {
			AugmentedStmt as = (AugmentedStmt) it.next();
			// System.out.println("Removed dominated stmt: "+as);
			synchBody.remove(as);
		}
	}

	private boolean verify_CatchBody(ExceptionNode en, IterableSet synchBody,
			Value monitorVariable, Value copiedLocal) {
		// System.out.println("starting verification");
		{
			/*
			 * synchBody is a likely superset of exception Node since the
			 * synchBody contains a goto stmt to the stmt right after the
			 * "to be created synch block" See if this is the case and remove
			 * the stmt
			 */

			IterableSet tryBodySet = en.get_TryBody();
			Iterator tempIt = tryBodySet.iterator();
			AugmentedStmt tempas = null;

			// to compute last stmt in a tryBody one should find the stmt whose
			// sucessor is not in the tryBody
			outer: while (tempIt.hasNext()) {
				tempas = (AugmentedStmt) tempIt.next();

				// get natural sucessors
				Iterator succIt = tempas.bsuccs.iterator();
				while (succIt.hasNext()) {
					AugmentedStmt succAS = (AugmentedStmt) succIt.next();
					if (!tryBodySet.contains(succAS)) {
						// tempas has a sucessor which is not part of the
						// trybody hence this is the last stmt
						break outer;
					}
				}
				// System.out.println(tempas);
			}

			// tempas contains the last augmentedStmt
			if (tempas != null) {

				// retrieving successors
				Iterator sit = tempas.bsuccs.iterator();
				while (sit.hasNext()) {
					AugmentedStmt sas = (AugmentedStmt) sit.next();
					// System.out.println("Removing: successor of last stmt:"+sas.get_Stmt());

					// this is the stmt which is the successor of the try block
					// which shouldnt be in the synchronized block
					// remove the stmt if present in synchBody

					synchBody.remove(sas);
					// System.out.println("Here, removed: "+sas);
					// should remove all other stmts in the synchBody which are
					// dominated by this stmt
					removeOtherDominatedStmts(synchBody, sas);
				}
			}
		}

		/*
		 * In the abc created code when a synch body occurs within a try block
		 * There is an error because the synchBody created has addition
		 * statements regarding the catching of exception due to the outer try
		 * block
		 * 
		 * Since these statements are not part of the synch body they should be
		 * removed
		 */
		{
			Iterator tempIt = en.get_TryBody().iterator();
			while (tempIt.hasNext()) {
				AugmentedStmt as = (AugmentedStmt) tempIt.next();
				if (as.get_Stmt() instanceof ExitMonitorStmt) {
					// System.out.println("All possible sucessors of as (CSUCCS):"+as.csuccs);
					List csuccs = as.csuccs;

					// remove the natural sucessors
					csuccs.remove(as.bsuccs);
					// now csuccs have the exception sucessors
					// System.out.println("Exception sucessors of Exit (CSUCCS:"+csuccs);

					Iterator succIt = csuccs.iterator();
					while (succIt.hasNext()) {
						AugmentedStmt as1 = (AugmentedStmt) succIt.next();
						if (as1.get_Stmt() instanceof GotoStmt) {
							Unit target = ((soot.jimple.internal.JGotoStmt) as1
									.get_Stmt()).getTarget();
							if (target instanceof DefinitionStmt) {
								DefinitionStmt defStmt = (DefinitionStmt) target;

								/*
								 * These are the caught exceptions (can be more
								 * than once if there are multiple areas of
								 * protection Keep the one which is of type
								 * Throwable
								 */

								Value asnFrom = defStmt.getRightOp();

								// if not a caught exception of type throwable
								// remove from synch
								if (!(asnFrom instanceof CaughtExceptionRef)) {
									// System.out.println("REMOVING:"+defStmt+" since this is not a caughtexception def");
									synchBody.remove(as1);
									// should remove all other stmts in the
									// synchBody which are dominated by this
									// stmt
									removeOtherDominatedStmts(synchBody, as1);
								} else {
									Value leftOp = defStmt.getLeftOp();
									// System.out.println("the left op is:"+leftOp);

									/*
									 * Only keep this if it is of throwable type
									 */
									HashSet params = new HashSet();
									params.addAll(davaBody.get_CaughtRefs());

									Iterator localIt = davaBody.getLocals()
											.iterator();
									String typeName = "";
									while (localIt.hasNext()) {
										Local local = (Local) localIt.next();
										if (local.toString().compareTo(
												leftOp.toString()) == 0) {
											Type t = local.getType();

											typeName = t.toString();
											break;
										}
									}

									if (!(typeName.compareTo(THROWABLE) == 0)) {
										// System.out.println("REMOVING:"+defStmt+
										// " since the caughtException not throwable type");
										synchBody.remove(as1);
										// should remove all other stmts in the
										// synchBody which are dominated by this
										// stmt
										removeOtherDominatedStmts(synchBody,
												as1);
									} else {
										// System.out.println("KEEPING"+defStmt);
										// System.out.println((RefType)((CaughtExceptionRef)
										// asnFrom).getType());
									}
								}
							} else {
								// System.out.println("\n\nnot definition"+target);
								// System.out.println("Removed"+as1);
								synchBody.remove(as1);
								// System.out.println(as1.bsuccs.get(0));
								synchBody.remove(as1.bsuccs.get(0));
								// should remove all other stmts in the
								// synchBody which are dominated by this stmt
								removeOtherDominatedStmts(synchBody, as1);
							}
						}
					}
				}
			}
		}

		/*
		 * There might be some unwanted stmts in the synch body. These are
		 * likely to be stmts which have no predecessor in the synchbody. Remove
		 * these stmts. NOTE: the entry of the synchbody is a special case since
		 * its predecessor is also not going to be in the synchbody but we
		 * SHOULD not remove the entry point
		 */

		// find the entry point of synchbody
		/*
		 * One way of doing this is going through the synch body and finiding a
		 * stmt whose predecessor is an enter monitor stmt NOT present in the
		 * synchBody
		 */
		AugmentedStmt synchEnter = null;
		Iterator synchIt = synchBody.iterator();

		outerLoop: while (synchIt.hasNext()) {
			AugmentedStmt as = (AugmentedStmt) synchIt.next();

			Iterator pit = as.cpreds.iterator();
			while (pit.hasNext()) {
				AugmentedStmt pas = (AugmentedStmt) pit.next();

				if (synchBody.contains(pas) == false) {
					// the as stmt has a predecessor which is not part of the
					// synchBody
					Stmt pasStmt = pas.get_Stmt();
					if (pasStmt instanceof EnterMonitorStmt) {
						// found the entry point to the synchBody
						synchEnter = as;
						break outerLoop;
					}
				}
			}
		}

		if (synchEnter == null) {
			throw new RuntimeException(
					"Could not find enter stmt of the synchBody: "
							+ davaBody.getMethod().getSignature());
		}

		// System.out.println("Enter stmt of synchBody is:"+synchEnter);

		/*
		 * Now that we know the exception case we can go through the synchBody
		 * and remove all stmts whose predecessor does not belong to the
		 * synchBody
		 */

		boolean unChanged = false;
		while (!unChanged) {
			unChanged = true;
			List<AugmentedStmt> toRemove = new ArrayList<AugmentedStmt>();
			synchIt = synchBody.iterator();
			while (synchIt.hasNext()) {
				AugmentedStmt synchAs = (AugmentedStmt) synchIt.next();
				if (synchAs == synchEnter) {
					// entrypoint is an exception so just continue
					continue;
				}
				Iterator pit = synchAs.cpreds.iterator();
				boolean remove = true;
				while (pit.hasNext()) {
					AugmentedStmt pAs = (AugmentedStmt) pit.next();
					if (synchBody.contains(pAs)) {
						// one of the preds of this as is in the synchBody so
						// dont remove
						remove = false;
					}
				}// going through preds of the synchAs
				if (remove) {
					// all preds not present in synchBody
					toRemove.add(synchAs);
				}
			}// going through the synchBody
			if (toRemove.size() > 0) {
				// none of the preds of synchAs are in the synchBody hence this
				// stmt is unreachable
				synchBody.removeAll(toRemove);
				// System.out.println("Removing:"+toRemove+" since none of its preds are in the synchBody");
				unChanged = false;
			}
		}

		// see if the two bodies match
		if ((en.get_Body().equals(synchBody) == false)) {
			// System.out.println("returning unverified since synchBody does not match");
			// System.out.println("\n\nEN BODY:\n"+en.get_Body());
			// System.out.println("\n\nSYNCH BODY:\n"+synchBody);
			return false;
		}

		/*
		 * The two bodies match check if the exception thrown is of type
		 * "throwable" and that there is only one catchlist The reason for doing
		 * this is that synchronized blocks get converted to a try catch block
		 * with the catch , catching the throwable exception and this is the
		 * ONLY catch
		 */
		if ((en.get_Exception().getName().equals(THROWABLE) == false)
				|| (en.get_CatchList().size() > 1)) {
			// System.out.println("returning unverified here");
			return false;
		}

		// at this point we know that the two bodies match and that the en
		// exception is a throwable exception

		/*
		 * find the entry point of the catch boody The entry point of the catch
		 * body is the first stmt in the catchbody This can be found by finiding
		 * the stmt whose predecessor is not part of the catch body
		 */
		IterableSet catchBody = en.get_CatchBody();
		AugmentedStmt entryPoint = null;

		Iterator it = catchBody.iterator();
		catchBodyLoop: while (it.hasNext()) {
			AugmentedStmt as = (AugmentedStmt) it.next();

			Iterator pit = as.cpreds.iterator();
			while (pit.hasNext()) {
				AugmentedStmt pas = (AugmentedStmt) pit.next();

				if (catchBody.contains(pas) == false) {
					entryPoint = as;
					break catchBodyLoop;
				}
			}
		}

		// Horror upon horrors, what follows is a hard coded state machine.

		/*
		 * To verify the catchbody one has to go through the catchbody ONE stmt
		 * at a time. This is NOT a good approach as it is using PATTERN
		 * MATCHING
		 * 
		 * FIRST STEP Need to verify that the entrypoint stmt and any goto stmts
		 * following it all point to the entrypoint
		 */

		Unit entryPointTarget = null;
		if (entryPoint.get_Stmt() instanceof GotoStmt) {
			// System.out.println("Entry point is a goto stmt getting the target");
			entryPointTarget = ((soot.jimple.internal.JGotoStmt) entryPoint
					.get_Stmt()).getTarget();
		}

		AugmentedStmt as = entryPoint;
		if (as.bsuccs.size() != 1) {
			// System.out.println("here1");
			return false;
		}

		while (as.get_Stmt() instanceof GotoStmt) {
			as = (AugmentedStmt) as.bsuccs.get(0);
			// if ((as.bsuccs.size() != 1) || ((as != entryPoint) &&
			// (as.cpreds.size() != 1))) {
			// return false;
			// }
			if (as.bsuccs.size() != 1) {
				// System.out.println("here2a");
				return false;
			}
			if (entryPointTarget != null) {
				if ((as.get_Stmt() != entryPointTarget)
						&& (as.cpreds.size() != 1)) {
					if (as.cpreds.size() != 1) {
						// System.out.println("here2b");
						return false;
					}
				}
			} else {
				if ((as != entryPoint) && (as.cpreds.size() != 1)) {
					// System.out.println("here2c");
					return false;
				}
			}
		}

		// so now we are not at a goto stmt for sure
		// according to the creation pattern of the try catch block we should be
		// at the definition stmt
		// e.g. <var> := @caughtexception

		Stmt s = as.get_Stmt();

		if (!(s instanceof DefinitionStmt)) {
			// System.out.println("here3");
			return false;
		}

		DefinitionStmt ds = (DefinitionStmt) s;
		Value asnFrom = ds.getRightOp();

		// if not a caught exception of type throwable we have a problem
		if (!((asnFrom instanceof CaughtExceptionRef) && (((RefType) ((CaughtExceptionRef) asnFrom)
				.getType()).getSootClass().getName().equals(THROWABLE)))) {
			// System.out.println("here4");
			return false;
		}

		Value throwlocal = ds.getLeftOp();
		// System.out.println("Throw local is:"+throwlocal);

		/*
		 * The escuccs contains all the EXCEPTION SUCESSORS of the
		 * caughtexception stmt
		 */
		IterableSet esuccs = new IterableSet();
		esuccs.addAll(as.csuccs);
		esuccs.removeAll(as.bsuccs);

		// sucessor of definition stmt
		as = (AugmentedStmt) as.bsuccs.get(0);
		s = as.get_Stmt();

		// this COULD be a copy stmt in which case update the throwlocal
		while (s instanceof DefinitionStmt
				&& (((DefinitionStmt) s).getRightOp().toString()
						.compareTo(throwlocal.toString()) == 0)) {

			// System.out.println("copy stmt using throwLocal found");
			// System.out.println("Right op is :"+((DefinitionStmt)s).getRightOp());
			// return false;
			throwlocal = ((DefinitionStmt) s).getLeftOp();

			// the sucessor of this stmt MIGHT be the exitmonitor stmt
			as = (AugmentedStmt) as.bsuccs.get(0);
			s = as.get_Stmt();
		}

		if (as.bsuccs.size() != 1) {
			// should have one true sucessor
			// System.out.println("here5a");
			return false;
		}

		if (as.cpreds.size() != 1) {
			// should have one true predecessor
			// System.out.println("here5b");
			return false;
		}

		// need to check whether this stmt is protected by the same exception
		// block as the whole catchbody
		checkProtectionArea(as, ds);

		s = as.get_Stmt();
		if (!(s instanceof ExitMonitorStmt)) {
			// System.out.println("Not an exit monitor stmt"+s);
			return false;
		}

		if ((((ExitMonitorStmt) s).getOp() != monitorVariable)) {

			if ((((ExitMonitorStmt) s).getOp() != copiedLocal)) {
				// System.out.println("exit monitor variable does not match enter monitor variable");
				return false;
			}
		}

		// next stmt should be a throw stmt
		as = (AugmentedStmt) as.bsuccs.get(0);
		if ((as.bsuccs.size() != 0) || (as.cpreds.size() != 1)
				|| (verify_ESuccs(as, esuccs) == false)) {
			// System.out.println("here7");
			return false;
		}

		s = as.get_Stmt();

		if (!((s instanceof ThrowStmt) && (((ThrowStmt) s).getOp() == throwlocal))) {
			// System.out.println("here8"+s+" Throw local is:"+throwlocal);
			return false;
		}

		return true;
	}

	/*
	 * DefinitionStmt s is the start of the area of protection The exception
	 * sucessors of as should directly or indirectly point to s
	 */
	private boolean checkProtectionArea(AugmentedStmt as, DefinitionStmt s) {
		IterableSet esuccs = new IterableSet();
		esuccs.addAll(as.csuccs);
		esuccs.removeAll(as.bsuccs);

		// esuccs contains the exception sucessors of as
		// System.out.println("ESUCCS are:"+esuccs);

		Iterator it = esuccs.iterator();
		while (it.hasNext()) {
			// going through each exception sucessor
			AugmentedStmt tempas = (AugmentedStmt) it.next();
			Stmt temps = tempas.get_Stmt();
			if (temps instanceof GotoStmt) {
				Unit target = ((GotoStmt) temps).getTarget();
				if (target != s) {
					// System.out.println("DID NOT Match indirectly");
					return false;
				} else {
					// System.out.println("Matched indirectly");
				}
			} else {
				if (temps != s) {
					// System.out.println("DID NOT Match directly");
					return false;
				} else {
					// System.out.println("Matched directly");
				}
			}

		}
		return true;
	}

	private boolean verify_ESuccs(AugmentedStmt as, IterableSet ref) {
		IterableSet esuccs = new IterableSet();

		esuccs.addAll(as.csuccs);
		esuccs.removeAll(as.bsuccs);

		// System.out.println("ESUCCS are:"+esuccs);
		// System.out.println("ref are:"+ref);
		return esuccs.equals(ref);
	}

	/*
	 * Input: head: this is the monitor enter stmt synchSet: this contains all
	 * sucessors of head which have level greater or equal to the head
	 */
	private IterableSet get_BodyApproximation(AugmentedStmt head,
			IterableSet synchSet) {
		IterableSet body = (IterableSet) synchSet.clone();
		Value local = ((EnterMonitorStmt) head.get_Stmt()).getOp();
		Integer level = as2ml.get(head).get(local);

		// System.out.println("BODY"+body);
		body.remove(head);

		Iterator bit = body.snapshotIterator();
		while (bit.hasNext()) {
			AugmentedStmt as = (AugmentedStmt) bit.next();
			Stmt s = as.get_Stmt();

			if ((s instanceof ExitMonitorStmt)
					&& (((ExitMonitorStmt) s).getOp() == local)
					&& ((as2ml.get(as).get(local)).equals(level))) {

				Iterator sit = as.csuccs.iterator();
				while (sit.hasNext()) {
					AugmentedStmt sas = (AugmentedStmt) sit.next();

					// if not dominated by head continue with next stmt in body
					if (sas.get_Dominators().contains(head) == false)
						continue;

					Stmt ss = sas.get_Stmt();

					if (((ss instanceof GotoStmt) || (ss instanceof ThrowStmt))
							&& (body.contains(sas) == false)) {
						// if (ss instanceof ThrowStmt && (body.contains( sas)
						// == false)){
						// System.out.println("adding"+sas);
						body.add(sas);
					}
				}
			}
		}

		return body;
	}
}
